[O] adding rudimentary support for Coq code blocks

[Eric Schulte]

See the attached example file.  This is very rudimentary, only
supporting session evaluation and without support for smart translation
between Org-mode and Coq data structures.

See the attached example file.

Coq http://coq.inria.fr/

1. Require supporting libraries.
   #+begin_src coq
     Require Import Bool.
     Require Import Arith.
     Require Import List.
   #+end_src

   #+RESULTS:
   : 

2. Simple function.
   #+begin_src coq
   (* Check if a list is sorted *)
   Fixpoint sortp (l : list nat) := match l with
       a :: b :: rst => if leb a b then sortp rst else false
     | a :: nil => true
     | nil => true
   end
   #+end_src

   #+RESULTS:
   : sortp is recursively defined (decreasing on 1st argument)
   : 

3. Run the above function.
   #+begin_src coq
     Eval compute in sortp (1::2::3::nil)
   #+end_src

   #+RESULTS:
   :      = true
   :      : bool
   : 

-- 
Eric Schulte
https://cs.unm.edu/~eschulte
PGP: 0x614CA05D